package ca.shojaei.mini_sat;


import java.util.Vector;



abstract public class Clause {

	
	protected boolean evaluable;
	protected boolean unary;
	protected boolean negated = false;
	private Clause right = null;
	private Clause left = null;
	
	public Clause(){}

	public boolean isEvaluable() {
		return evaluable;
	}

	public void setEvaluable(boolean evaluable) {
		this.evaluable = evaluable;
	}
	
	public boolean isUnary() {
		return unary;
	}

	public void setUnary(boolean unary) {
		this.unary = unary;
	}	

	public abstract boolean evaluate( Model m);
	

	abstract String getSymbol();

	public boolean isNegated() {
		return negated;
	}

	public void setNegated(boolean negated) {
		this.negated = negated;
	}
	
	public abstract Clause getRight();
	public abstract Clause getLeft();
	
	public abstract void setRight( Clause c);
	public abstract void setLeft(Clause c);
	
	public abstract Vector<int[]> getDIMACS(Model m);
	
	protected Vector<int[]> and(Vector<int[]> e1, Vector<int[]> e2)
	{
		Vector<int[]> result = new Vector<int[]>();
		
		for(int i = 0; i < e1.size(); i++)
		{
            if(!SAT.contain(result, e1.get(i)))			
            	result.add(e1.get(i));
		}
		
		for(int i = 0; i < e2.size(); i++)
		{
			if(!SAT.contain(result, e2.get(i)))
				result.add(e2.get(i));
		}
		
		
		return result;
	}
	
	protected Vector<int[]> or(Vector<int[]> e1, Vector<int[]> e2)
	{
		
		Vector<int[]> v = new Vector<int[]>();
	
		for(int i = 0; i < e1.size() ; i++){
			for(int j = 0; j < e2.size(); j++)
			{
				int[] temp = new int[e1.get(i).length + e2.get(j).length];
				int counter = 0;
				for(int m = 0 ; m < e1.get(i).length ; m++)
				{
					assert(counter < temp.length);
					temp[counter] = e1.get(i)[m];
					counter++;
					
				}
				for(int m = 0 ; m < e2.get(j).length ; m++)
				{
					assert(counter < temp.length);
					temp[counter] = e2.get(j)[m];
					counter++;
				}
				if(!SAT.contain(v, temp))
					v.add(temp);
			}
		}
		
		return v;
	}
	
}
